﻿using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;

namespace TruthTree2.PC.Logic
{
    public class Negation : Sentence
    {
        internal Sentence inner;

        public Negation(Sentence o)
        {
            inner = o;
        }

        public override int SortValue
        {
            get
            {
                if (inner is Conjunction) { return 2; }
                if (inner is Biconditional) { return 2; }
                if (inner is Atom) { return 0; }

                return 1;
            }
        }
        public override bool Decomposable
        {
            get
            {
                if (inner is Atom) { return false; }

                return true;
            }
        }

        public override Sentence Copy()
        {
            return new Negation(inner.Copy());
        }

        public override Decomposition GetDecomposition()
        {
            Decomposition decomp = new Decomposition();

            if (inner is Atom) { }
            else if (inner is Biconditional)
            {
                Biconditional b = (Biconditional)inner;
                decomp.AddToLeft(b.left.Copy());
                decomp.AddToLeft(b.right.GetNegation());
                decomp.AddToRight(b.left.GetNegation());
                decomp.AddToRight(b.right.Copy());
            }
            else if (inner is Conditional)
            {
                Conditional c = (Conditional)inner;
                decomp.AddToLeft(c.antecedent.Copy());
                decomp.AddToLeft(c.consequent.GetNegation());
            }
            else if (inner is Conjunction)
            {
                Conjunction c = (Conjunction)inner;
                decomp.AddToLeft(c.left.GetNegation());
                decomp.AddToRight(c.right.GetNegation());
            }
            else if (inner is Disjunction)
            {
                Disjunction d = (Disjunction)inner;
                decomp.AddToLeft(d.left.GetNegation());
                decomp.AddToLeft(d.right.GetNegation());
            }
            else if (inner is Negation)
            {
                Negation n = (Negation)inner;
                decomp.AddToLeft(n.inner.Copy());
            }

            return decomp;
        }

        new public Sentence GetNegation()
        {
            return inner.Copy();
        }

        public override bool Equal(Sentence o)
        {
            if (o is Negation)
            {
                Negation n = (Negation)o;
                return inner.Equal(n.inner);
            }

            return false;
        }

        public override string ToString()
        {
            return "(not " + inner.ToString() + ")";
        }
    }
}
